(0) Obligation:
Clauses:
ss(Xs, Ys) :- ','(perm(Xs, Ys), ordered(Ys)).
perm([], []).
perm(Xs, .(X, Ys)) :- ','(app(X1s, .(X, X2s), Xs), ','(app(X1s, X2s, Zs), perm(Zs, Ys))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
ordered([]).
ordered(.(X1, [])).
ordered(.(X, .(Y, Xs))) :- ','(less(X, s(Y)), ordered(.(Y, Xs))).
less(0, s(X2)).
less(s(X), s(Y)) :- less(X, Y).
Query: ss(g,g)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
appA(.(X1, X2), X3, X4, .(X1, X5)) :- appA(X2, X3, X4, X5).
appB(.(X1, X2), X3, .(X1, X4)) :- appB(X2, X3, X4).
permC(X1, .(X2, X3)) :- appA(X4, X2, X5, X1).
permC(X1, .(X2, X3)) :- ','(appcA(X4, X2, X5, X1), appB(X4, X5, X6)).
permC(X1, .(X2, X3)) :- ','(appcA(X4, X2, X5, X1), ','(appcB(X4, X5, X6), permC(X6, X3))).
orderedD(s(X1), .(X2, X3)) :- lessF(X1, X2).
orderedD(X1, .(X2, X3)) :- ','(lesscE(X1, X2), orderedD(X2, X3)).
lessF(s(X1), s(X2)) :- lessF(X1, X2).
ssG(X1, .(X2, X3)) :- appA(X4, X2, X5, X1).
ssG(X1, .(X2, X3)) :- ','(appcA(X4, X2, X5, X1), appB(X4, X5, X6)).
ssG(X1, .(X2, X3)) :- ','(appcA(X4, X2, X5, X1), ','(appcB(X4, X5, X6), permC(X6, X3))).
ssG(X1, .(X2, X3)) :- ','(appcA(X4, X2, X5, X1), ','(appcB(X4, X5, X6), ','(permcC(X6, X3), orderedD(X2, X3)))).
Clauses:
appcA([], X1, X2, .(X1, X2)).
appcA(.(X1, X2), X3, X4, .(X1, X5)) :- appcA(X2, X3, X4, X5).
appcB([], X1, X1).
appcB(.(X1, X2), X3, .(X1, X4)) :- appcB(X2, X3, X4).
permcC([], []).
permcC(X1, .(X2, X3)) :- ','(appcA(X4, X2, X5, X1), ','(appcB(X4, X5, X6), permcC(X6, X3))).
orderedcD(X1, []).
orderedcD(X1, .(X2, X3)) :- ','(lesscE(X1, X2), orderedcD(X2, X3)).
lesscF(0, s(X1)).
lesscF(s(X1), s(X2)) :- lesscF(X1, X2).
lesscE(0, X1).
lesscE(s(X1), X2) :- lesscF(X1, X2).
Afs:
ssG(x1, x2) = ssG(x1, x2)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
ssG_in: (b,b)
appA_in: (f,b,f,b)
appcA_in: (f,b,f,b)
appB_in: (b,b,f)
appcB_in: (b,b,f)
permC_in: (b,b)
permcC_in: (b,b)
orderedD_in: (b,b)
lessF_in: (b,b)
lesscE_in: (b,b)
lesscF_in: (b,b)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
SSG_IN_GG(X1, .(X2, X3)) → U12_GG(X1, X2, X3, appA_in_agag(X4, X2, X5, X1))
SSG_IN_GG(X1, .(X2, X3)) → APPA_IN_AGAG(X4, X2, X5, X1)
APPA_IN_AGAG(.(X1, X2), X3, X4, .(X1, X5)) → U1_AGAG(X1, X2, X3, X4, X5, appA_in_agag(X2, X3, X4, X5))
APPA_IN_AGAG(.(X1, X2), X3, X4, .(X1, X5)) → APPA_IN_AGAG(X2, X3, X4, X5)
SSG_IN_GG(X1, .(X2, X3)) → U13_GG(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U13_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U14_GG(X1, X2, X3, appB_in_gga(X4, X5, X6))
U13_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → APPB_IN_GGA(X4, X5, X6)
APPB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U2_GGA(X1, X2, X3, X4, appB_in_gga(X2, X3, X4))
APPB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPB_IN_GGA(X2, X3, X4)
U13_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U15_GG(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U15_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U16_GG(X1, X2, X3, permC_in_gg(X6, X3))
U15_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → PERMC_IN_GG(X6, X3)
PERMC_IN_GG(X1, .(X2, X3)) → U3_GG(X1, X2, X3, appA_in_agag(X4, X2, X5, X1))
PERMC_IN_GG(X1, .(X2, X3)) → APPA_IN_AGAG(X4, X2, X5, X1)
PERMC_IN_GG(X1, .(X2, X3)) → U4_GG(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U4_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U5_GG(X1, X2, X3, appB_in_gga(X4, X5, X6))
U4_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → APPB_IN_GGA(X4, X5, X6)
U4_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U6_GG(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U6_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U7_GG(X1, X2, X3, permC_in_gg(X6, X3))
U6_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → PERMC_IN_GG(X6, X3)
U15_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U17_GG(X1, X2, X3, permcC_in_gg(X6, X3))
U17_GG(X1, X2, X3, permcC_out_gg(X6, X3)) → U18_GG(X1, X2, X3, orderedD_in_gg(X2, X3))
U17_GG(X1, X2, X3, permcC_out_gg(X6, X3)) → ORDEREDD_IN_GG(X2, X3)
ORDEREDD_IN_GG(s(X1), .(X2, X3)) → U8_GG(X1, X2, X3, lessF_in_gg(X1, X2))
ORDEREDD_IN_GG(s(X1), .(X2, X3)) → LESSF_IN_GG(X1, X2)
LESSF_IN_GG(s(X1), s(X2)) → U11_GG(X1, X2, lessF_in_gg(X1, X2))
LESSF_IN_GG(s(X1), s(X2)) → LESSF_IN_GG(X1, X2)
ORDEREDD_IN_GG(X1, .(X2, X3)) → U9_GG(X1, X2, X3, lesscE_in_gg(X1, X2))
U9_GG(X1, X2, X3, lesscE_out_gg(X1, X2)) → U10_GG(X1, X2, X3, orderedD_in_gg(X2, X3))
U9_GG(X1, X2, X3, lesscE_out_gg(X1, X2)) → ORDEREDD_IN_GG(X2, X3)
The TRS R consists of the following rules:
appcA_in_agag([], X1, X2, .(X1, X2)) → appcA_out_agag([], X1, X2, .(X1, X2))
appcA_in_agag(.(X1, X2), X3, X4, .(X1, X5)) → U20_agag(X1, X2, X3, X4, X5, appcA_in_agag(X2, X3, X4, X5))
U20_agag(X1, X2, X3, X4, X5, appcA_out_agag(X2, X3, X4, X5)) → appcA_out_agag(.(X1, X2), X3, X4, .(X1, X5))
appcB_in_gga([], X1, X1) → appcB_out_gga([], X1, X1)
appcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U21_gga(X1, X2, X3, X4, appcB_in_gga(X2, X3, X4))
U21_gga(X1, X2, X3, X4, appcB_out_gga(X2, X3, X4)) → appcB_out_gga(.(X1, X2), X3, .(X1, X4))
permcC_in_gg([], []) → permcC_out_gg([], [])
permcC_in_gg(X1, .(X2, X3)) → U22_gg(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U22_gg(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U23_gg(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U23_gg(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U24_gg(X1, X2, X3, permcC_in_gg(X6, X3))
U24_gg(X1, X2, X3, permcC_out_gg(X6, X3)) → permcC_out_gg(X1, .(X2, X3))
lesscE_in_gg(0, X1) → lesscE_out_gg(0, X1)
lesscE_in_gg(s(X1), X2) → U28_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lesscF_in_gg(X1, X2))
U27_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U28_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(X1), X2)
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
appA_in_agag(
x1,
x2,
x3,
x4) =
appA_in_agag(
x2,
x4)
appcA_in_agag(
x1,
x2,
x3,
x4) =
appcA_in_agag(
x2,
x4)
appcA_out_agag(
x1,
x2,
x3,
x4) =
appcA_out_agag(
x1,
x2,
x3,
x4)
U20_agag(
x1,
x2,
x3,
x4,
x5,
x6) =
U20_agag(
x1,
x3,
x5,
x6)
appB_in_gga(
x1,
x2,
x3) =
appB_in_gga(
x1,
x2)
appcB_in_gga(
x1,
x2,
x3) =
appcB_in_gga(
x1,
x2)
[] =
[]
appcB_out_gga(
x1,
x2,
x3) =
appcB_out_gga(
x1,
x2,
x3)
U21_gga(
x1,
x2,
x3,
x4,
x5) =
U21_gga(
x1,
x2,
x3,
x5)
permC_in_gg(
x1,
x2) =
permC_in_gg(
x1,
x2)
permcC_in_gg(
x1,
x2) =
permcC_in_gg(
x1,
x2)
permcC_out_gg(
x1,
x2) =
permcC_out_gg(
x1,
x2)
U22_gg(
x1,
x2,
x3,
x4) =
U22_gg(
x1,
x2,
x3,
x4)
U23_gg(
x1,
x2,
x3,
x4) =
U23_gg(
x1,
x2,
x3,
x4)
U24_gg(
x1,
x2,
x3,
x4) =
U24_gg(
x1,
x2,
x3,
x4)
orderedD_in_gg(
x1,
x2) =
orderedD_in_gg(
x1,
x2)
s(
x1) =
s(
x1)
lessF_in_gg(
x1,
x2) =
lessF_in_gg(
x1,
x2)
lesscE_in_gg(
x1,
x2) =
lesscE_in_gg(
x1,
x2)
0 =
0
lesscE_out_gg(
x1,
x2) =
lesscE_out_gg(
x1,
x2)
U28_gg(
x1,
x2,
x3) =
U28_gg(
x1,
x2,
x3)
lesscF_in_gg(
x1,
x2) =
lesscF_in_gg(
x1,
x2)
lesscF_out_gg(
x1,
x2) =
lesscF_out_gg(
x1,
x2)
U27_gg(
x1,
x2,
x3) =
U27_gg(
x1,
x2,
x3)
SSG_IN_GG(
x1,
x2) =
SSG_IN_GG(
x1,
x2)
U12_GG(
x1,
x2,
x3,
x4) =
U12_GG(
x1,
x2,
x3,
x4)
APPA_IN_AGAG(
x1,
x2,
x3,
x4) =
APPA_IN_AGAG(
x2,
x4)
U1_AGAG(
x1,
x2,
x3,
x4,
x5,
x6) =
U1_AGAG(
x1,
x3,
x5,
x6)
U13_GG(
x1,
x2,
x3,
x4) =
U13_GG(
x1,
x2,
x3,
x4)
U14_GG(
x1,
x2,
x3,
x4) =
U14_GG(
x1,
x2,
x3,
x4)
APPB_IN_GGA(
x1,
x2,
x3) =
APPB_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4,
x5) =
U2_GGA(
x1,
x2,
x3,
x5)
U15_GG(
x1,
x2,
x3,
x4) =
U15_GG(
x1,
x2,
x3,
x4)
U16_GG(
x1,
x2,
x3,
x4) =
U16_GG(
x1,
x2,
x3,
x4)
PERMC_IN_GG(
x1,
x2) =
PERMC_IN_GG(
x1,
x2)
U3_GG(
x1,
x2,
x3,
x4) =
U3_GG(
x1,
x2,
x3,
x4)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x1,
x2,
x3,
x4)
U5_GG(
x1,
x2,
x3,
x4) =
U5_GG(
x1,
x2,
x3,
x4)
U6_GG(
x1,
x2,
x3,
x4) =
U6_GG(
x1,
x2,
x3,
x4)
U7_GG(
x1,
x2,
x3,
x4) =
U7_GG(
x1,
x2,
x3,
x4)
U17_GG(
x1,
x2,
x3,
x4) =
U17_GG(
x1,
x2,
x3,
x4)
U18_GG(
x1,
x2,
x3,
x4) =
U18_GG(
x1,
x2,
x3,
x4)
ORDEREDD_IN_GG(
x1,
x2) =
ORDEREDD_IN_GG(
x1,
x2)
U8_GG(
x1,
x2,
x3,
x4) =
U8_GG(
x1,
x2,
x3,
x4)
LESSF_IN_GG(
x1,
x2) =
LESSF_IN_GG(
x1,
x2)
U11_GG(
x1,
x2,
x3) =
U11_GG(
x1,
x2,
x3)
U9_GG(
x1,
x2,
x3,
x4) =
U9_GG(
x1,
x2,
x3,
x4)
U10_GG(
x1,
x2,
x3,
x4) =
U10_GG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SSG_IN_GG(X1, .(X2, X3)) → U12_GG(X1, X2, X3, appA_in_agag(X4, X2, X5, X1))
SSG_IN_GG(X1, .(X2, X3)) → APPA_IN_AGAG(X4, X2, X5, X1)
APPA_IN_AGAG(.(X1, X2), X3, X4, .(X1, X5)) → U1_AGAG(X1, X2, X3, X4, X5, appA_in_agag(X2, X3, X4, X5))
APPA_IN_AGAG(.(X1, X2), X3, X4, .(X1, X5)) → APPA_IN_AGAG(X2, X3, X4, X5)
SSG_IN_GG(X1, .(X2, X3)) → U13_GG(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U13_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U14_GG(X1, X2, X3, appB_in_gga(X4, X5, X6))
U13_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → APPB_IN_GGA(X4, X5, X6)
APPB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U2_GGA(X1, X2, X3, X4, appB_in_gga(X2, X3, X4))
APPB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPB_IN_GGA(X2, X3, X4)
U13_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U15_GG(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U15_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U16_GG(X1, X2, X3, permC_in_gg(X6, X3))
U15_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → PERMC_IN_GG(X6, X3)
PERMC_IN_GG(X1, .(X2, X3)) → U3_GG(X1, X2, X3, appA_in_agag(X4, X2, X5, X1))
PERMC_IN_GG(X1, .(X2, X3)) → APPA_IN_AGAG(X4, X2, X5, X1)
PERMC_IN_GG(X1, .(X2, X3)) → U4_GG(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U4_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U5_GG(X1, X2, X3, appB_in_gga(X4, X5, X6))
U4_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → APPB_IN_GGA(X4, X5, X6)
U4_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U6_GG(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U6_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U7_GG(X1, X2, X3, permC_in_gg(X6, X3))
U6_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → PERMC_IN_GG(X6, X3)
U15_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U17_GG(X1, X2, X3, permcC_in_gg(X6, X3))
U17_GG(X1, X2, X3, permcC_out_gg(X6, X3)) → U18_GG(X1, X2, X3, orderedD_in_gg(X2, X3))
U17_GG(X1, X2, X3, permcC_out_gg(X6, X3)) → ORDEREDD_IN_GG(X2, X3)
ORDEREDD_IN_GG(s(X1), .(X2, X3)) → U8_GG(X1, X2, X3, lessF_in_gg(X1, X2))
ORDEREDD_IN_GG(s(X1), .(X2, X3)) → LESSF_IN_GG(X1, X2)
LESSF_IN_GG(s(X1), s(X2)) → U11_GG(X1, X2, lessF_in_gg(X1, X2))
LESSF_IN_GG(s(X1), s(X2)) → LESSF_IN_GG(X1, X2)
ORDEREDD_IN_GG(X1, .(X2, X3)) → U9_GG(X1, X2, X3, lesscE_in_gg(X1, X2))
U9_GG(X1, X2, X3, lesscE_out_gg(X1, X2)) → U10_GG(X1, X2, X3, orderedD_in_gg(X2, X3))
U9_GG(X1, X2, X3, lesscE_out_gg(X1, X2)) → ORDEREDD_IN_GG(X2, X3)
The TRS R consists of the following rules:
appcA_in_agag([], X1, X2, .(X1, X2)) → appcA_out_agag([], X1, X2, .(X1, X2))
appcA_in_agag(.(X1, X2), X3, X4, .(X1, X5)) → U20_agag(X1, X2, X3, X4, X5, appcA_in_agag(X2, X3, X4, X5))
U20_agag(X1, X2, X3, X4, X5, appcA_out_agag(X2, X3, X4, X5)) → appcA_out_agag(.(X1, X2), X3, X4, .(X1, X5))
appcB_in_gga([], X1, X1) → appcB_out_gga([], X1, X1)
appcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U21_gga(X1, X2, X3, X4, appcB_in_gga(X2, X3, X4))
U21_gga(X1, X2, X3, X4, appcB_out_gga(X2, X3, X4)) → appcB_out_gga(.(X1, X2), X3, .(X1, X4))
permcC_in_gg([], []) → permcC_out_gg([], [])
permcC_in_gg(X1, .(X2, X3)) → U22_gg(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U22_gg(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U23_gg(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U23_gg(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U24_gg(X1, X2, X3, permcC_in_gg(X6, X3))
U24_gg(X1, X2, X3, permcC_out_gg(X6, X3)) → permcC_out_gg(X1, .(X2, X3))
lesscE_in_gg(0, X1) → lesscE_out_gg(0, X1)
lesscE_in_gg(s(X1), X2) → U28_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lesscF_in_gg(X1, X2))
U27_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U28_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(X1), X2)
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
appA_in_agag(
x1,
x2,
x3,
x4) =
appA_in_agag(
x2,
x4)
appcA_in_agag(
x1,
x2,
x3,
x4) =
appcA_in_agag(
x2,
x4)
appcA_out_agag(
x1,
x2,
x3,
x4) =
appcA_out_agag(
x1,
x2,
x3,
x4)
U20_agag(
x1,
x2,
x3,
x4,
x5,
x6) =
U20_agag(
x1,
x3,
x5,
x6)
appB_in_gga(
x1,
x2,
x3) =
appB_in_gga(
x1,
x2)
appcB_in_gga(
x1,
x2,
x3) =
appcB_in_gga(
x1,
x2)
[] =
[]
appcB_out_gga(
x1,
x2,
x3) =
appcB_out_gga(
x1,
x2,
x3)
U21_gga(
x1,
x2,
x3,
x4,
x5) =
U21_gga(
x1,
x2,
x3,
x5)
permC_in_gg(
x1,
x2) =
permC_in_gg(
x1,
x2)
permcC_in_gg(
x1,
x2) =
permcC_in_gg(
x1,
x2)
permcC_out_gg(
x1,
x2) =
permcC_out_gg(
x1,
x2)
U22_gg(
x1,
x2,
x3,
x4) =
U22_gg(
x1,
x2,
x3,
x4)
U23_gg(
x1,
x2,
x3,
x4) =
U23_gg(
x1,
x2,
x3,
x4)
U24_gg(
x1,
x2,
x3,
x4) =
U24_gg(
x1,
x2,
x3,
x4)
orderedD_in_gg(
x1,
x2) =
orderedD_in_gg(
x1,
x2)
s(
x1) =
s(
x1)
lessF_in_gg(
x1,
x2) =
lessF_in_gg(
x1,
x2)
lesscE_in_gg(
x1,
x2) =
lesscE_in_gg(
x1,
x2)
0 =
0
lesscE_out_gg(
x1,
x2) =
lesscE_out_gg(
x1,
x2)
U28_gg(
x1,
x2,
x3) =
U28_gg(
x1,
x2,
x3)
lesscF_in_gg(
x1,
x2) =
lesscF_in_gg(
x1,
x2)
lesscF_out_gg(
x1,
x2) =
lesscF_out_gg(
x1,
x2)
U27_gg(
x1,
x2,
x3) =
U27_gg(
x1,
x2,
x3)
SSG_IN_GG(
x1,
x2) =
SSG_IN_GG(
x1,
x2)
U12_GG(
x1,
x2,
x3,
x4) =
U12_GG(
x1,
x2,
x3,
x4)
APPA_IN_AGAG(
x1,
x2,
x3,
x4) =
APPA_IN_AGAG(
x2,
x4)
U1_AGAG(
x1,
x2,
x3,
x4,
x5,
x6) =
U1_AGAG(
x1,
x3,
x5,
x6)
U13_GG(
x1,
x2,
x3,
x4) =
U13_GG(
x1,
x2,
x3,
x4)
U14_GG(
x1,
x2,
x3,
x4) =
U14_GG(
x1,
x2,
x3,
x4)
APPB_IN_GGA(
x1,
x2,
x3) =
APPB_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4,
x5) =
U2_GGA(
x1,
x2,
x3,
x5)
U15_GG(
x1,
x2,
x3,
x4) =
U15_GG(
x1,
x2,
x3,
x4)
U16_GG(
x1,
x2,
x3,
x4) =
U16_GG(
x1,
x2,
x3,
x4)
PERMC_IN_GG(
x1,
x2) =
PERMC_IN_GG(
x1,
x2)
U3_GG(
x1,
x2,
x3,
x4) =
U3_GG(
x1,
x2,
x3,
x4)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x1,
x2,
x3,
x4)
U5_GG(
x1,
x2,
x3,
x4) =
U5_GG(
x1,
x2,
x3,
x4)
U6_GG(
x1,
x2,
x3,
x4) =
U6_GG(
x1,
x2,
x3,
x4)
U7_GG(
x1,
x2,
x3,
x4) =
U7_GG(
x1,
x2,
x3,
x4)
U17_GG(
x1,
x2,
x3,
x4) =
U17_GG(
x1,
x2,
x3,
x4)
U18_GG(
x1,
x2,
x3,
x4) =
U18_GG(
x1,
x2,
x3,
x4)
ORDEREDD_IN_GG(
x1,
x2) =
ORDEREDD_IN_GG(
x1,
x2)
U8_GG(
x1,
x2,
x3,
x4) =
U8_GG(
x1,
x2,
x3,
x4)
LESSF_IN_GG(
x1,
x2) =
LESSF_IN_GG(
x1,
x2)
U11_GG(
x1,
x2,
x3) =
U11_GG(
x1,
x2,
x3)
U9_GG(
x1,
x2,
x3,
x4) =
U9_GG(
x1,
x2,
x3,
x4)
U10_GG(
x1,
x2,
x3,
x4) =
U10_GG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 22 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LESSF_IN_GG(s(X1), s(X2)) → LESSF_IN_GG(X1, X2)
The TRS R consists of the following rules:
appcA_in_agag([], X1, X2, .(X1, X2)) → appcA_out_agag([], X1, X2, .(X1, X2))
appcA_in_agag(.(X1, X2), X3, X4, .(X1, X5)) → U20_agag(X1, X2, X3, X4, X5, appcA_in_agag(X2, X3, X4, X5))
U20_agag(X1, X2, X3, X4, X5, appcA_out_agag(X2, X3, X4, X5)) → appcA_out_agag(.(X1, X2), X3, X4, .(X1, X5))
appcB_in_gga([], X1, X1) → appcB_out_gga([], X1, X1)
appcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U21_gga(X1, X2, X3, X4, appcB_in_gga(X2, X3, X4))
U21_gga(X1, X2, X3, X4, appcB_out_gga(X2, X3, X4)) → appcB_out_gga(.(X1, X2), X3, .(X1, X4))
permcC_in_gg([], []) → permcC_out_gg([], [])
permcC_in_gg(X1, .(X2, X3)) → U22_gg(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U22_gg(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U23_gg(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U23_gg(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U24_gg(X1, X2, X3, permcC_in_gg(X6, X3))
U24_gg(X1, X2, X3, permcC_out_gg(X6, X3)) → permcC_out_gg(X1, .(X2, X3))
lesscE_in_gg(0, X1) → lesscE_out_gg(0, X1)
lesscE_in_gg(s(X1), X2) → U28_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lesscF_in_gg(X1, X2))
U27_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U28_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(X1), X2)
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
appcA_in_agag(
x1,
x2,
x3,
x4) =
appcA_in_agag(
x2,
x4)
appcA_out_agag(
x1,
x2,
x3,
x4) =
appcA_out_agag(
x1,
x2,
x3,
x4)
U20_agag(
x1,
x2,
x3,
x4,
x5,
x6) =
U20_agag(
x1,
x3,
x5,
x6)
appcB_in_gga(
x1,
x2,
x3) =
appcB_in_gga(
x1,
x2)
[] =
[]
appcB_out_gga(
x1,
x2,
x3) =
appcB_out_gga(
x1,
x2,
x3)
U21_gga(
x1,
x2,
x3,
x4,
x5) =
U21_gga(
x1,
x2,
x3,
x5)
permcC_in_gg(
x1,
x2) =
permcC_in_gg(
x1,
x2)
permcC_out_gg(
x1,
x2) =
permcC_out_gg(
x1,
x2)
U22_gg(
x1,
x2,
x3,
x4) =
U22_gg(
x1,
x2,
x3,
x4)
U23_gg(
x1,
x2,
x3,
x4) =
U23_gg(
x1,
x2,
x3,
x4)
U24_gg(
x1,
x2,
x3,
x4) =
U24_gg(
x1,
x2,
x3,
x4)
s(
x1) =
s(
x1)
lesscE_in_gg(
x1,
x2) =
lesscE_in_gg(
x1,
x2)
0 =
0
lesscE_out_gg(
x1,
x2) =
lesscE_out_gg(
x1,
x2)
U28_gg(
x1,
x2,
x3) =
U28_gg(
x1,
x2,
x3)
lesscF_in_gg(
x1,
x2) =
lesscF_in_gg(
x1,
x2)
lesscF_out_gg(
x1,
x2) =
lesscF_out_gg(
x1,
x2)
U27_gg(
x1,
x2,
x3) =
U27_gg(
x1,
x2,
x3)
LESSF_IN_GG(
x1,
x2) =
LESSF_IN_GG(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LESSF_IN_GG(s(X1), s(X2)) → LESSF_IN_GG(X1, X2)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LESSF_IN_GG(s(X1), s(X2)) → LESSF_IN_GG(X1, X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- LESSF_IN_GG(s(X1), s(X2)) → LESSF_IN_GG(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
(13) YES
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
ORDEREDD_IN_GG(X1, .(X2, X3)) → U9_GG(X1, X2, X3, lesscE_in_gg(X1, X2))
U9_GG(X1, X2, X3, lesscE_out_gg(X1, X2)) → ORDEREDD_IN_GG(X2, X3)
The TRS R consists of the following rules:
appcA_in_agag([], X1, X2, .(X1, X2)) → appcA_out_agag([], X1, X2, .(X1, X2))
appcA_in_agag(.(X1, X2), X3, X4, .(X1, X5)) → U20_agag(X1, X2, X3, X4, X5, appcA_in_agag(X2, X3, X4, X5))
U20_agag(X1, X2, X3, X4, X5, appcA_out_agag(X2, X3, X4, X5)) → appcA_out_agag(.(X1, X2), X3, X4, .(X1, X5))
appcB_in_gga([], X1, X1) → appcB_out_gga([], X1, X1)
appcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U21_gga(X1, X2, X3, X4, appcB_in_gga(X2, X3, X4))
U21_gga(X1, X2, X3, X4, appcB_out_gga(X2, X3, X4)) → appcB_out_gga(.(X1, X2), X3, .(X1, X4))
permcC_in_gg([], []) → permcC_out_gg([], [])
permcC_in_gg(X1, .(X2, X3)) → U22_gg(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U22_gg(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U23_gg(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U23_gg(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U24_gg(X1, X2, X3, permcC_in_gg(X6, X3))
U24_gg(X1, X2, X3, permcC_out_gg(X6, X3)) → permcC_out_gg(X1, .(X2, X3))
lesscE_in_gg(0, X1) → lesscE_out_gg(0, X1)
lesscE_in_gg(s(X1), X2) → U28_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lesscF_in_gg(X1, X2))
U27_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U28_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(X1), X2)
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
appcA_in_agag(
x1,
x2,
x3,
x4) =
appcA_in_agag(
x2,
x4)
appcA_out_agag(
x1,
x2,
x3,
x4) =
appcA_out_agag(
x1,
x2,
x3,
x4)
U20_agag(
x1,
x2,
x3,
x4,
x5,
x6) =
U20_agag(
x1,
x3,
x5,
x6)
appcB_in_gga(
x1,
x2,
x3) =
appcB_in_gga(
x1,
x2)
[] =
[]
appcB_out_gga(
x1,
x2,
x3) =
appcB_out_gga(
x1,
x2,
x3)
U21_gga(
x1,
x2,
x3,
x4,
x5) =
U21_gga(
x1,
x2,
x3,
x5)
permcC_in_gg(
x1,
x2) =
permcC_in_gg(
x1,
x2)
permcC_out_gg(
x1,
x2) =
permcC_out_gg(
x1,
x2)
U22_gg(
x1,
x2,
x3,
x4) =
U22_gg(
x1,
x2,
x3,
x4)
U23_gg(
x1,
x2,
x3,
x4) =
U23_gg(
x1,
x2,
x3,
x4)
U24_gg(
x1,
x2,
x3,
x4) =
U24_gg(
x1,
x2,
x3,
x4)
s(
x1) =
s(
x1)
lesscE_in_gg(
x1,
x2) =
lesscE_in_gg(
x1,
x2)
0 =
0
lesscE_out_gg(
x1,
x2) =
lesscE_out_gg(
x1,
x2)
U28_gg(
x1,
x2,
x3) =
U28_gg(
x1,
x2,
x3)
lesscF_in_gg(
x1,
x2) =
lesscF_in_gg(
x1,
x2)
lesscF_out_gg(
x1,
x2) =
lesscF_out_gg(
x1,
x2)
U27_gg(
x1,
x2,
x3) =
U27_gg(
x1,
x2,
x3)
ORDEREDD_IN_GG(
x1,
x2) =
ORDEREDD_IN_GG(
x1,
x2)
U9_GG(
x1,
x2,
x3,
x4) =
U9_GG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(15) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
ORDEREDD_IN_GG(X1, .(X2, X3)) → U9_GG(X1, X2, X3, lesscE_in_gg(X1, X2))
U9_GG(X1, X2, X3, lesscE_out_gg(X1, X2)) → ORDEREDD_IN_GG(X2, X3)
The TRS R consists of the following rules:
lesscE_in_gg(0, X1) → lesscE_out_gg(0, X1)
lesscE_in_gg(s(X1), X2) → U28_gg(X1, X2, lesscF_in_gg(X1, X2))
U28_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(X1), X2)
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lesscF_in_gg(X1, X2))
U27_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
Pi is empty.
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ORDEREDD_IN_GG(X1, .(X2, X3)) → U9_GG(X1, X2, X3, lesscE_in_gg(X1, X2))
U9_GG(X1, X2, X3, lesscE_out_gg(X1, X2)) → ORDEREDD_IN_GG(X2, X3)
The TRS R consists of the following rules:
lesscE_in_gg(0, X1) → lesscE_out_gg(0, X1)
lesscE_in_gg(s(X1), X2) → U28_gg(X1, X2, lesscF_in_gg(X1, X2))
U28_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(X1), X2)
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lesscF_in_gg(X1, X2))
U27_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
The set Q consists of the following terms:
lesscE_in_gg(x0, x1)
U28_gg(x0, x1, x2)
lesscF_in_gg(x0, x1)
U27_gg(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(19) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- U9_GG(X1, X2, X3, lesscE_out_gg(X1, X2)) → ORDEREDD_IN_GG(X2, X3)
The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2
- ORDEREDD_IN_GG(X1, .(X2, X3)) → U9_GG(X1, X2, X3, lesscE_in_gg(X1, X2))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
(20) YES
(21) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPB_IN_GGA(X2, X3, X4)
The TRS R consists of the following rules:
appcA_in_agag([], X1, X2, .(X1, X2)) → appcA_out_agag([], X1, X2, .(X1, X2))
appcA_in_agag(.(X1, X2), X3, X4, .(X1, X5)) → U20_agag(X1, X2, X3, X4, X5, appcA_in_agag(X2, X3, X4, X5))
U20_agag(X1, X2, X3, X4, X5, appcA_out_agag(X2, X3, X4, X5)) → appcA_out_agag(.(X1, X2), X3, X4, .(X1, X5))
appcB_in_gga([], X1, X1) → appcB_out_gga([], X1, X1)
appcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U21_gga(X1, X2, X3, X4, appcB_in_gga(X2, X3, X4))
U21_gga(X1, X2, X3, X4, appcB_out_gga(X2, X3, X4)) → appcB_out_gga(.(X1, X2), X3, .(X1, X4))
permcC_in_gg([], []) → permcC_out_gg([], [])
permcC_in_gg(X1, .(X2, X3)) → U22_gg(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U22_gg(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U23_gg(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U23_gg(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U24_gg(X1, X2, X3, permcC_in_gg(X6, X3))
U24_gg(X1, X2, X3, permcC_out_gg(X6, X3)) → permcC_out_gg(X1, .(X2, X3))
lesscE_in_gg(0, X1) → lesscE_out_gg(0, X1)
lesscE_in_gg(s(X1), X2) → U28_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lesscF_in_gg(X1, X2))
U27_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U28_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(X1), X2)
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
appcA_in_agag(
x1,
x2,
x3,
x4) =
appcA_in_agag(
x2,
x4)
appcA_out_agag(
x1,
x2,
x3,
x4) =
appcA_out_agag(
x1,
x2,
x3,
x4)
U20_agag(
x1,
x2,
x3,
x4,
x5,
x6) =
U20_agag(
x1,
x3,
x5,
x6)
appcB_in_gga(
x1,
x2,
x3) =
appcB_in_gga(
x1,
x2)
[] =
[]
appcB_out_gga(
x1,
x2,
x3) =
appcB_out_gga(
x1,
x2,
x3)
U21_gga(
x1,
x2,
x3,
x4,
x5) =
U21_gga(
x1,
x2,
x3,
x5)
permcC_in_gg(
x1,
x2) =
permcC_in_gg(
x1,
x2)
permcC_out_gg(
x1,
x2) =
permcC_out_gg(
x1,
x2)
U22_gg(
x1,
x2,
x3,
x4) =
U22_gg(
x1,
x2,
x3,
x4)
U23_gg(
x1,
x2,
x3,
x4) =
U23_gg(
x1,
x2,
x3,
x4)
U24_gg(
x1,
x2,
x3,
x4) =
U24_gg(
x1,
x2,
x3,
x4)
s(
x1) =
s(
x1)
lesscE_in_gg(
x1,
x2) =
lesscE_in_gg(
x1,
x2)
0 =
0
lesscE_out_gg(
x1,
x2) =
lesscE_out_gg(
x1,
x2)
U28_gg(
x1,
x2,
x3) =
U28_gg(
x1,
x2,
x3)
lesscF_in_gg(
x1,
x2) =
lesscF_in_gg(
x1,
x2)
lesscF_out_gg(
x1,
x2) =
lesscF_out_gg(
x1,
x2)
U27_gg(
x1,
x2,
x3) =
U27_gg(
x1,
x2,
x3)
APPB_IN_GGA(
x1,
x2,
x3) =
APPB_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(22) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(23) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPB_IN_GGA(X2, X3, X4)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
APPB_IN_GGA(
x1,
x2,
x3) =
APPB_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(24) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APPB_IN_GGA(.(X1, X2), X3) → APPB_IN_GGA(X2, X3)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(26) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- APPB_IN_GGA(.(X1, X2), X3) → APPB_IN_GGA(X2, X3)
The graph contains the following edges 1 > 1, 2 >= 2
(27) YES
(28) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPA_IN_AGAG(.(X1, X2), X3, X4, .(X1, X5)) → APPA_IN_AGAG(X2, X3, X4, X5)
The TRS R consists of the following rules:
appcA_in_agag([], X1, X2, .(X1, X2)) → appcA_out_agag([], X1, X2, .(X1, X2))
appcA_in_agag(.(X1, X2), X3, X4, .(X1, X5)) → U20_agag(X1, X2, X3, X4, X5, appcA_in_agag(X2, X3, X4, X5))
U20_agag(X1, X2, X3, X4, X5, appcA_out_agag(X2, X3, X4, X5)) → appcA_out_agag(.(X1, X2), X3, X4, .(X1, X5))
appcB_in_gga([], X1, X1) → appcB_out_gga([], X1, X1)
appcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U21_gga(X1, X2, X3, X4, appcB_in_gga(X2, X3, X4))
U21_gga(X1, X2, X3, X4, appcB_out_gga(X2, X3, X4)) → appcB_out_gga(.(X1, X2), X3, .(X1, X4))
permcC_in_gg([], []) → permcC_out_gg([], [])
permcC_in_gg(X1, .(X2, X3)) → U22_gg(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U22_gg(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U23_gg(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U23_gg(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U24_gg(X1, X2, X3, permcC_in_gg(X6, X3))
U24_gg(X1, X2, X3, permcC_out_gg(X6, X3)) → permcC_out_gg(X1, .(X2, X3))
lesscE_in_gg(0, X1) → lesscE_out_gg(0, X1)
lesscE_in_gg(s(X1), X2) → U28_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lesscF_in_gg(X1, X2))
U27_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U28_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(X1), X2)
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
appcA_in_agag(
x1,
x2,
x3,
x4) =
appcA_in_agag(
x2,
x4)
appcA_out_agag(
x1,
x2,
x3,
x4) =
appcA_out_agag(
x1,
x2,
x3,
x4)
U20_agag(
x1,
x2,
x3,
x4,
x5,
x6) =
U20_agag(
x1,
x3,
x5,
x6)
appcB_in_gga(
x1,
x2,
x3) =
appcB_in_gga(
x1,
x2)
[] =
[]
appcB_out_gga(
x1,
x2,
x3) =
appcB_out_gga(
x1,
x2,
x3)
U21_gga(
x1,
x2,
x3,
x4,
x5) =
U21_gga(
x1,
x2,
x3,
x5)
permcC_in_gg(
x1,
x2) =
permcC_in_gg(
x1,
x2)
permcC_out_gg(
x1,
x2) =
permcC_out_gg(
x1,
x2)
U22_gg(
x1,
x2,
x3,
x4) =
U22_gg(
x1,
x2,
x3,
x4)
U23_gg(
x1,
x2,
x3,
x4) =
U23_gg(
x1,
x2,
x3,
x4)
U24_gg(
x1,
x2,
x3,
x4) =
U24_gg(
x1,
x2,
x3,
x4)
s(
x1) =
s(
x1)
lesscE_in_gg(
x1,
x2) =
lesscE_in_gg(
x1,
x2)
0 =
0
lesscE_out_gg(
x1,
x2) =
lesscE_out_gg(
x1,
x2)
U28_gg(
x1,
x2,
x3) =
U28_gg(
x1,
x2,
x3)
lesscF_in_gg(
x1,
x2) =
lesscF_in_gg(
x1,
x2)
lesscF_out_gg(
x1,
x2) =
lesscF_out_gg(
x1,
x2)
U27_gg(
x1,
x2,
x3) =
U27_gg(
x1,
x2,
x3)
APPA_IN_AGAG(
x1,
x2,
x3,
x4) =
APPA_IN_AGAG(
x2,
x4)
We have to consider all (P,R,Pi)-chains
(29) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(30) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPA_IN_AGAG(.(X1, X2), X3, X4, .(X1, X5)) → APPA_IN_AGAG(X2, X3, X4, X5)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
APPA_IN_AGAG(
x1,
x2,
x3,
x4) =
APPA_IN_AGAG(
x2,
x4)
We have to consider all (P,R,Pi)-chains
(31) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APPA_IN_AGAG(X3, .(X1, X5)) → APPA_IN_AGAG(X3, X5)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(33) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- APPA_IN_AGAG(X3, .(X1, X5)) → APPA_IN_AGAG(X3, X5)
The graph contains the following edges 1 >= 1, 2 > 2
(34) YES
(35) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PERMC_IN_GG(X1, .(X2, X3)) → U4_GG(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U4_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U6_GG(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U6_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → PERMC_IN_GG(X6, X3)
The TRS R consists of the following rules:
appcA_in_agag([], X1, X2, .(X1, X2)) → appcA_out_agag([], X1, X2, .(X1, X2))
appcA_in_agag(.(X1, X2), X3, X4, .(X1, X5)) → U20_agag(X1, X2, X3, X4, X5, appcA_in_agag(X2, X3, X4, X5))
U20_agag(X1, X2, X3, X4, X5, appcA_out_agag(X2, X3, X4, X5)) → appcA_out_agag(.(X1, X2), X3, X4, .(X1, X5))
appcB_in_gga([], X1, X1) → appcB_out_gga([], X1, X1)
appcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U21_gga(X1, X2, X3, X4, appcB_in_gga(X2, X3, X4))
U21_gga(X1, X2, X3, X4, appcB_out_gga(X2, X3, X4)) → appcB_out_gga(.(X1, X2), X3, .(X1, X4))
permcC_in_gg([], []) → permcC_out_gg([], [])
permcC_in_gg(X1, .(X2, X3)) → U22_gg(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U22_gg(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U23_gg(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U23_gg(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → U24_gg(X1, X2, X3, permcC_in_gg(X6, X3))
U24_gg(X1, X2, X3, permcC_out_gg(X6, X3)) → permcC_out_gg(X1, .(X2, X3))
lesscE_in_gg(0, X1) → lesscE_out_gg(0, X1)
lesscE_in_gg(s(X1), X2) → U28_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lesscF_in_gg(X1, X2))
U27_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U28_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(X1), X2)
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
appcA_in_agag(
x1,
x2,
x3,
x4) =
appcA_in_agag(
x2,
x4)
appcA_out_agag(
x1,
x2,
x3,
x4) =
appcA_out_agag(
x1,
x2,
x3,
x4)
U20_agag(
x1,
x2,
x3,
x4,
x5,
x6) =
U20_agag(
x1,
x3,
x5,
x6)
appcB_in_gga(
x1,
x2,
x3) =
appcB_in_gga(
x1,
x2)
[] =
[]
appcB_out_gga(
x1,
x2,
x3) =
appcB_out_gga(
x1,
x2,
x3)
U21_gga(
x1,
x2,
x3,
x4,
x5) =
U21_gga(
x1,
x2,
x3,
x5)
permcC_in_gg(
x1,
x2) =
permcC_in_gg(
x1,
x2)
permcC_out_gg(
x1,
x2) =
permcC_out_gg(
x1,
x2)
U22_gg(
x1,
x2,
x3,
x4) =
U22_gg(
x1,
x2,
x3,
x4)
U23_gg(
x1,
x2,
x3,
x4) =
U23_gg(
x1,
x2,
x3,
x4)
U24_gg(
x1,
x2,
x3,
x4) =
U24_gg(
x1,
x2,
x3,
x4)
s(
x1) =
s(
x1)
lesscE_in_gg(
x1,
x2) =
lesscE_in_gg(
x1,
x2)
0 =
0
lesscE_out_gg(
x1,
x2) =
lesscE_out_gg(
x1,
x2)
U28_gg(
x1,
x2,
x3) =
U28_gg(
x1,
x2,
x3)
lesscF_in_gg(
x1,
x2) =
lesscF_in_gg(
x1,
x2)
lesscF_out_gg(
x1,
x2) =
lesscF_out_gg(
x1,
x2)
U27_gg(
x1,
x2,
x3) =
U27_gg(
x1,
x2,
x3)
PERMC_IN_GG(
x1,
x2) =
PERMC_IN_GG(
x1,
x2)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x1,
x2,
x3,
x4)
U6_GG(
x1,
x2,
x3,
x4) =
U6_GG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(36) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(37) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PERMC_IN_GG(X1, .(X2, X3)) → U4_GG(X1, X2, X3, appcA_in_agag(X4, X2, X5, X1))
U4_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U6_GG(X1, X2, X3, appcB_in_gga(X4, X5, X6))
U6_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → PERMC_IN_GG(X6, X3)
The TRS R consists of the following rules:
appcA_in_agag([], X1, X2, .(X1, X2)) → appcA_out_agag([], X1, X2, .(X1, X2))
appcA_in_agag(.(X1, X2), X3, X4, .(X1, X5)) → U20_agag(X1, X2, X3, X4, X5, appcA_in_agag(X2, X3, X4, X5))
appcB_in_gga([], X1, X1) → appcB_out_gga([], X1, X1)
appcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U21_gga(X1, X2, X3, X4, appcB_in_gga(X2, X3, X4))
U20_agag(X1, X2, X3, X4, X5, appcA_out_agag(X2, X3, X4, X5)) → appcA_out_agag(.(X1, X2), X3, X4, .(X1, X5))
U21_gga(X1, X2, X3, X4, appcB_out_gga(X2, X3, X4)) → appcB_out_gga(.(X1, X2), X3, .(X1, X4))
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
appcA_in_agag(
x1,
x2,
x3,
x4) =
appcA_in_agag(
x2,
x4)
appcA_out_agag(
x1,
x2,
x3,
x4) =
appcA_out_agag(
x1,
x2,
x3,
x4)
U20_agag(
x1,
x2,
x3,
x4,
x5,
x6) =
U20_agag(
x1,
x3,
x5,
x6)
appcB_in_gga(
x1,
x2,
x3) =
appcB_in_gga(
x1,
x2)
[] =
[]
appcB_out_gga(
x1,
x2,
x3) =
appcB_out_gga(
x1,
x2,
x3)
U21_gga(
x1,
x2,
x3,
x4,
x5) =
U21_gga(
x1,
x2,
x3,
x5)
PERMC_IN_GG(
x1,
x2) =
PERMC_IN_GG(
x1,
x2)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x1,
x2,
x3,
x4)
U6_GG(
x1,
x2,
x3,
x4) =
U6_GG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(38) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(39) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PERMC_IN_GG(X1, .(X2, X3)) → U4_GG(X1, X2, X3, appcA_in_agag(X2, X1))
U4_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U6_GG(X1, X2, X3, appcB_in_gga(X4, X5))
U6_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → PERMC_IN_GG(X6, X3)
The TRS R consists of the following rules:
appcA_in_agag(X1, .(X1, X2)) → appcA_out_agag([], X1, X2, .(X1, X2))
appcA_in_agag(X3, .(X1, X5)) → U20_agag(X1, X3, X5, appcA_in_agag(X3, X5))
appcB_in_gga([], X1) → appcB_out_gga([], X1, X1)
appcB_in_gga(.(X1, X2), X3) → U21_gga(X1, X2, X3, appcB_in_gga(X2, X3))
U20_agag(X1, X3, X5, appcA_out_agag(X2, X3, X4, X5)) → appcA_out_agag(.(X1, X2), X3, X4, .(X1, X5))
U21_gga(X1, X2, X3, appcB_out_gga(X2, X3, X4)) → appcB_out_gga(.(X1, X2), X3, .(X1, X4))
The set Q consists of the following terms:
appcA_in_agag(x0, x1)
appcB_in_gga(x0, x1)
U20_agag(x0, x1, x2, x3)
U21_gga(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(40) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- U4_GG(X1, X2, X3, appcA_out_agag(X4, X2, X5, X1)) → U6_GG(X1, X2, X3, appcB_in_gga(X4, X5))
The graph contains the following edges 1 >= 1, 4 > 1, 2 >= 2, 4 > 2, 3 >= 3
- U6_GG(X1, X2, X3, appcB_out_gga(X4, X5, X6)) → PERMC_IN_GG(X6, X3)
The graph contains the following edges 4 > 1, 3 >= 2
- PERMC_IN_GG(X1, .(X2, X3)) → U4_GG(X1, X2, X3, appcA_in_agag(X2, X1))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
(41) YES